MIME-Version: 1.0
Server: CERN/3.0
Date: Monday, 25-Nov-96 00:40:53 GMT
Content-Type: text/html
Content-Length: 20145
Last-Modified: Sunday, 29-Sep-96 20:50:30 GMT

<TITLE>Nuprl Project Related Publications</TITLE>
<!body bgcolor="#ffffff">
<!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><img src="http://www.cs.cornell.edu/Info/Projects/NuPrl/icons/line.red.right.gif">

<H1>Nuprl Project Related Web Sites</H1>

<UL>
	<li><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><a href=http://www.altavista.digital.com/cgi-bin/query?pg=q&what=web&fmt=.&q=Nuprl> AltaVista(tm) Search</a>
	<LI> <!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><A HREF="http://www.cs.cornell.edu/Info/People/jackson/nuprl/index.html">	Paul Jackson's Nuprl Page</A>
</UL>

<!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><img src="http://www.cs.cornell.edu/Info/Projects/NuPrl/icons/line.red.right.gif">


<H1>Nuprl Project Online Papers</H1>

There are several formats used to present the papers accessible here.
<OL>
<LI> HTML : A hypertext version created using <!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><A HREF="http://cbl.leeds.ac.uk/nikos/tex2html/doc/latex2html/latex2html.html"> latex2html. </A>
<LI> PostScript : A downloadable PostScript version created using dvips.
<LI> NCSTRL : A pointer into the <!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><A HREF="http://cs-tr.cs.cornell.edu/"> Networked Computer Science Technical Reports Library. </A>
</OL>

<HR>

<UL>
<LI> Collaborative Mathematics Environments.
	[<!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><A HREF="http://www.cs.cornell.edu/Info/Projects/NuPrl/documents/colmath/it.html"> HTML </A>, 
         <!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><A HREF="http://www.cs.cornell.edu/Info/Projects/NuPrl/documents/colmath.ps"> PostScript </A>]
<LI> Constable, R.
<UL> <LI> Experience Using Type Theory as a Foundation for Computer Science, circa 1985-1995.
        [<!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><A HREF="http://www.cs.cornell.edu/Info/Projects/NuPrl/documents/make/make.html">HTML </A>]
</UL>

<LI> Constable, R.
<UL> <LI> Semantics of Evidence.
	[<!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><A HREF="http://www.cs.cornell.edu/Info/Projects/NuPrl/documents/semantics/it.html"> HTML </A>,
	 <!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><A HREF="http://cs-tr.cs.cornell.edu:80/Dienst/UI/2.0/Describe/ncstrl.cornell%2fTR85-684"> NCSTRL </A>]
</UL>
<LI> Constable, R.
<UL> <LI> The Value of Automated Deductions.
        [<!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><A HREF="http://www.cs.cornell.edu/Info/Projects/NuPrl/documents/deduction/deduction.html">HTML </A>]
</UL>    
<LI> Forester, M.
<UL> <LI> Formalizing Constructive Real Analysis.
	[<!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><A HREF="http://www.cs.cornell.edu/Info/Projects/NuPrl/documents/real-analysis/it.html"> HTML </A>,
	 <!WA13><!WA13><!WA13><!WA13><!WA13><!WA13><!WA13><!WA13><!WA13><!WA13><!WA13><!WA13><A HREF="http://cs-tr.cs.cornell.edu:80/Dienst/UI/2.0/Describe/ncstrl.cornell%2fTR93-1382"> NCSTRL </A>,
         <!WA14><!WA14><!WA14><!WA14><!WA14><!WA14><!WA14><!WA14><!WA14><!WA14><!WA14><!WA14><A HREF="http://www.cs.cornell.edu/Info/Projects/NuPrl/documents/real-analysis.ps"> PostScript </A>]
</UL>
</UL> 

<!WA15><!WA15><!WA15><!WA15><!WA15><!WA15><!WA15><!WA15><!WA15><!WA15><!WA15><!WA15><img src="http://www.cs.cornell.edu/Info/Projects/NuPrl/icons/line.red.right.gif">

<H1>Nuprl Project Related Publications</H1>

<ul>
   <li> <b>Published Papers and Chapters of Books</b>
     <p>
     <ol>
	<li>
	<font color="#ee0000">Aagaard, Mark and Leeser, Miriam,</font>
	<i>Verifying a Logic Synthesis Tool in Nuprl.</i>
	<b>Proceedings of Workshop on Computer-Aided Verification.</b>
	1992.
	Editor: Gregor Bochmann and David Probst,
	Publisher: Springer-Verlag,
	pp. 72-83.
	(To appear by Springer-Verlag, 1993)

	<li>
 	<font color="#ee0000">Allen, Stuart F. and Robert L. Constable and Douglas J. Howe and Willaim Aitken.</font>
	<i>The Semantics of Reflected Proof.</i>
	<b>Proc. of Fifth Symp. on Logic in Comp. Sci.</b>
	IEEE, 
	1990,
	pp. 95-197

	<li>
	<font color="#ee0000">Allen, Stuart F.</font>
	<i>A Non-Type-Theoretic Definition of Martin-Lof's Types.</i>
	<b>Proc. of Second Symp. on Logic in Comp. Sci.</b>
	IEEE,
	June 1987,
	pp. 215-224
       
	<li>
        <font color="#ee0000">Allen, Stuart F.</font>
        <i>A non-type-theoretic semantics for type-theoretic language.</i>
        <b>Cornell University.</b>
        1987

	<li>
	<font color="#ee0000">Basin, David A.</font>
	<i>Extracting circuits from constructive proofs.</i>
	<b>Dept. of Artificial Intelligence, Edinburgh.</b>
	1991,
	Research Paper 533,
	(Also appeared in Proc. of the IFIP-IEEE Int'l. Workshop on Form
	al Methods in VLSI Design, Miami USA, 1991.)


	<li>
	<font color="#ee0000">Basin, David A. and Douglas J.Howe,</font>
	<i>Some Normalization Properties of Martin-Lof's Type Theory, and Applications,</i>
	<b>Theoretical Aspects of Computer Software, Int. Conf. TACS '91,</b>
	(Lecture Notes in Computer Science, Vol. 526})
	Springer-Verlag,
	pp. 475-494,
	1991

	<li>
	<font color="#ee0000">Basin, D. and G. Brown and M. Leeser,</font>
	<i>Formally Verified Synthesis of Combinational Circuits,</i>
	<b>Integration: The International Journal of  VLSI Design,</b>
	1991,
	v. 11,
	pp. 235-250

       	<li>
	<font color="#ee0000">Basin, D. and R. Constable,</font>
	<i>Metalogical Frameworks,</i>
	<b>Proc. of the Second Annual Workshop on Logical Frameworks,</b>
	Edinburgh, UK,
	June 1991
	
	<li>
	<font color="#ee0000">Basin, David A.,</font>
	<i>Building Problem Solving Environments in Constructive Type Theory,</i>
	<b>Cornell University,</b>
	1990"

	<li>
	<font color="#ee0000">Basin, D. and P. Del Vecchio</font>
	<i>Hardware Specification, Verification and Synthesis,</i>
	<b>Hardware Specification, Verification and Synthesis:  Mathematical Aspects,</b>
	(Lecture Notes in Computer Science, Vol. 408)
	1989,
	pp. 333-357,
	Springer-Verlag

	<li>
	<font color="#ee0000">Basin, David A.,</font>
	<i>Building Theories in Nuprl,</i>
	<b>Proc. of Logic at Botik '89,</b>
	(Lecture Notes in Computer Science, Vol. 363),
	pp. 12-25,
	Springer-Verlag, Pereslavl-Zalesky, USSR,
	1989,
	(Cornell TR 88-932)

	<li>
	<font color="#ee0000">Basin, David A.,</font>
	<i>An environment for automated reasoning about partial functions</i>,
	<b>9th International Conference on Automated Deduction,</b>
	(Lecture Notes in Computer Science, Vol. 310),
	pp. 101-110,
	Springer-Verlag, NY,
	1988

	<li>
        <font color="#ee0000">Bates, J. L. and Robert L. Constable,</font>
        <i>Proofs as programs,</i>
        <b>ACM Trans. Program. Lang. and Syst.,</b>
	v. 7,
	n. 1,
	pp. 53-71,
	1985

	<li>
	<font color="#ee0000">Bundy, A. and F. van Harmelen and C. Horn and A. Smaill,</font>
	<i>The Oyster-Clam system,</i>
	<b>10th International Conference on Automated Design,</b>
	(Lecture Notes in Artificial Intelligence, Vol. 449),
	Springer-Verlag,
	1990,
	Stickel, M.E. (Editor),
	pp. 647-648

	<li>
	<font color="#ee0000">Chen, W.Z.,</font>
	<i>Tactic-based Theorem Proving and Knowledge-based Forward Chaining,</i>
	<b>Eleventh International Conference on Automated Deduction,</b>
	(Lecture Notes in A.I., Vol. 607),
	1992,
	D. Kapur (Editor),
	pp. 552-566,
	Springer-Verlag
	
	<li>
	<font color="#ee0000">Chirimar, J. and Douglas J.~Howe,</font>
	<i>Implementing Constructive Real Analysis: a Preliminary Report,</i>
	<b>Symposium on Constructivity in Computer Science,</b>
	Springer-Verlag,
	1991

	<li>
	<font color="#ee0000">Robert L. Constable,</font>
	<i>Exporting and reflecting abstract constructive meta-mathematics,</i>
	<b>Lecture Notes in Artificial Intelligence,</b>
	1994,
	Alan Bundy (Editor),
	p. 529,
	(12th International Conference on Automated Deduction),
	Springer-Verlag

        <li>
	<font color="#ee0000">Robert L. Constable,</font>
	<i>Expressing computational complexity in constructive type theory,</i>
        <b>LNCS/LNAI Proceedings, </b>
        (Lecture Notes in Computer Science),
        1994,
	pp. 131-144,
        Springer-Verlag

	<li>
	<font color="#ee0000">Robert L. Constable,</font>
	<i>Using Reflection to Explain and Enhance Type Theory</i>,
	<b>Proof and Computation</b>,
	1994,
	NATO ASI Series,
	Springer-Verlag

	<li>
	<font color="#ee0000">Constable, Robert L. and Paul B. Jackson,</font>
	<i>Towards Integrated Systems for Symbolic Algebra and Formal Constructive Mathematics,</i>
	To appear.,
	1994

	<li>
	<font color="#ee0000">Constable, Robert L. and Scott F. Smith,</font>
	<i>Computational Foundations of Basic Recursive Function Theory,</i>
	<b>Theoretical Computer Science B: Logic, semantics, and theory of programming,</b>
	1993,
	v. 121,
	pp. 89-112

	<li>
	<font color="#ee0000">Constable, Robert L.,</font>
	<i>Formal Theories and Software Systems:  
	Fundamental Connections between Computer Science and Logic,</i>
	<b>Future Tendencies in Computer Science, Control and Applied Mathematics,</b>
	(Lecture Notes in Computer Science, Vol. 653),
	Springer-Verlag,
	December, 1992,
	Bensoussan, A. and J.-P. Verjus (Editors),
	pp. 105-127

	<li>
	<font color="#ee0000">Constable, Robert L.,</font>
	<i>Metalevel Programming in Constructive Type Theory,</i>
	<b>Programming and Mathematical Method,</b>
	(NATO ASI Series, Vol. F88),
	Springer-Verlag,
	1992,
	Broy, Manfred (Editor),
	pp. 45-93

	<li>
	<font color="#ee0000">Constable, Robert L.,</font>
	<i>Lectures on: Classical Proofs as Programs,</i>
	<b>Constructive Methods of Computing Science,</b>
	(NATO ASI Series),
	M. Broy (Editor),
	1992

	<li>
	<font color="#ee0000">Constable, Robert L. and Chetan Murthy,</font>
	<i>Finding  Computational Content from Classical Proofs,</i>
	<b>Logical Frameworks,</b>
	Cambridge University Press,
	1991,
	Gerard Huet and Gordon Plotkin (Editors),
	pp. 341-362

	<li>
	<font color="#ee0000">Constable, Robert L.,</font>
	<i>Type Theory as a Foundation for Computer Science,</i>
	<b>Theoretical Aspects of Computer Software, Int. Conf. TACS '91,</b>
	(Lecture Notes in Computer Science, Vol. 526),
	1991,
	pp. 226-243

	<li>
	<font color="#ee0000">Constable, Robert L. and  Stuart F. Allen and Douglas J. Howe,</font>
	<i>Reflecting the Open-Ended Computation System of Constructive Type  Theory,</i>
	<b>Logic, Algebra and Computation,</b>
	(NATO ASI Series, Vol. F79),
	H. Schwichtenberg (Editor),
	1990

	<li>
        <font color="#ee0000">Robert L. Constable and Douglas J. Howe,</font>
        <i>Implementing Metamathematics as an Approach to Automatic Theorem Proving,</i>
        <b>Formal Techniques in Artificial Intelligence: A Source Book,</b>
        Elsevier Science Publishers (North-Holland),
        1990,
        R.B. Banerji (Editor),
        pp. 45-76

	<li>
	<font color="#ee0000">Constable, Robert L. and Douglas J. Howe,</font>
	<i>Nuprl as a General Logic,</i>
	<b>Logic in Computer Science,</b>
	Academic Press,
	1990,
	P. Odifreddi (Editor),
	pp. 77-90,
	(Cornell TR 89-1021)

	<li>
	<font color="#ee0000">Constable, Robert L.,</font>
	<i>Assigning Meaning to Proofs: a semantic basis for problem solving environments,</i>
	<b>Constructive Methods of Computing Science,</b>
	(NATO ASI Series, Vol. F55),
	M. Broy (Editor),
	pp. 63-91,
	1989 

	<li>
	<font color="#ee0000">Constable, Robert L. and Scott F. Smith,</font>
	<i>Computational Foundations of Basic Recursive Function Theory,</i>
	<b>Third Symp. on Logic in Comp. Sci.,</b>
	IEEE, Edinburgh, UK,
	pp. 360-371,
	1988,
	(Cornell TR 88-904)

	<li>
	<font color="#ee0000">Constable, Robert L. and Stuart F. Allen and H.M. Bromley and W.R. Cleaveland 
	and J.F. Cremer and R.W. Harper and Douglas J. Howe and T.B. Knoblock and 
	N.P. Mendler and P. Panangaden and James T. Sasaki and Scott F. Smith,</font>
	<b>Implementing Mathematics with the Nuprl Development System,</b>
	Prentice-Hall, NJ,
	1986

	<li>
	<font color="#ee0000">Constable, Robert L. and N.P. Mendler,</font>
	<i>Recursive Definitions in Type Theory,</i>
	<b>Proc. of Logics of Prog. Conf.,</b>
	pp. 61-78,
	January 1985,
	(Cornell TR 85-659)

	<li>
	<font color="#ee0000">Constable, Robert L.,</font>
	<i>Constructive Mathematics as a programming logic:  some principles of theory,</i>
	<b>Annals of Mathematics,</b>
	Vol. 24,
	Elsevier Science Publishers, B.V. (North-Holland),
	1985,
	(Reprinted from 
		<i>Topics in the Theory of Computation, </i>
		<b> Selected Papers of the Intnl. Conf. on "Foundations of Computation Theory," FCT '83</b>
	)

	<li>
	<font color="#ee0000">Constable, Robert L. and T. Knoblock and J.L. Bates,</font>
	<i>Writing programs that construct proofs,</i>
	<b>J. Automated Reasoning,</b>
	v. 1,
	n. 3,
	pp. 285-326,
	1984

	<li>
	<font color="#ee0000">Constable, Robert L. and Michael J. O'Donnell,</font>
        <b>A Programming Logic</b>,
        Winthrop, Mass,
        1978

	<li>	
        <font color="#ee0000">Constable, Robert L.,</font>
        <i>Constructive mathematics and automatic program writers,</i>
        <b>Proc. IFIP Congr.,</b>
        Ljubljana,
	pp. 229-233,
        1971

	<li>
	<font color="#ee0000">Giunchiglia, F. and A. Smaill,</font>
	<i>Reflection in constrcutive and non-constructive automated reasoning,</i>
	<b>Meta-Programming in Logic Programming,</b>
	MIT Press,
	1989,
	Abramson, H. and M.H. Rogers (Editors),
	pp. 123-140

	<li>
	<font color="#ee0000">Horn, C.,</font>
	<i>The Nuprl proof development system,</i>
	<b>Dept. of Artificial Intelligence, Edinburgh,</b>
	1988,
	Working paper 214

        <li>
	<font color="#ee0000">Howe, Douglas J.and Stoller, Scott D.,</font>
        <i>An operational approach to combining classical set theory and functional programming languages, </i>
        <b>International Symposium TACS '94,</b>
        (Lecture Notes in Computer Science),
        Springer-Verlag,
        1994,
	Goos, G. and Hartmanis, J. (Editors),
        pp. 36-55

	<li>
	<font color="#ee0000">Howe, Douglas J.,</font>
	<i>Reasoning About Functional Programs in Nuprl,</i>
	<b>Functional Programming, Concurrency, Simulation and Automated Reasoning,</b>
	(Lecture Notes in Computer Science),
	1993,
	(To appear)

	<li>
	<font color="#ee0000">Howe, Douglas J.,</font>
	<b>A Simple Type Theory for Reasoning about Functional Programs.</b>
	Computer Science Department, Cornell Univeristy,
	(Pre print),
	1992

	<li>
	<font color="#ee0000">Howe, Douglas J.,</font>
	<i>Equality in Lazy Computation Systems,</i>
	<b>Proc. of Fourth Symp. on Logic in Comp. Sci.,</b>
	1989,
	IEEE Computer Society,
	pp. 198-203

	<li>
	<font color="#ee0000">Howe, Douglas J.,</font>
	<i>Computational Metatheory in Nuprl,</i>
	<b>9th International Conference on Automated Deduction,</b>
	(Lecture Notes in Computer Science, Vol. 310),
	E. Lusk and R. Overbeek (Editors),
	pp. 238-257,
	Springer-Verlag, New York,
	1988

	<li>
	<font color="#ee0000">Howe, Douglas J.,</font>
	<b>Automating Reasoning in an Implementation of Constructive Type Theory</b>,
	Cornell University,
	1988

	<li>
	<font color="#ee0000">Howe, Douglas J.</font>
	<i>Implementing Number Theory: An Experiment with Nuprl,</i>
	<b>8th International Conference on Automated Deduction,</b>
	(Lecture Notes in Computer Science, Vol. 230),
	1987,
	pp. 404-415

	<li>
	<font color="#ee0000">Howe, Douglas J.</font>
	<i>The Computational Behaviour of Girard's Paradox</i>
	<b>Proc. of Second Symp. on Logic in Comp. Sci.</b>
	IEEE,
	1987,
	pp. 205--214

	<li>
	<font color="#ee0000">Jackson, Paul B. and Robert L. Constable,</font>
	<i>Type Theory for Computer Algebra,</i>
	(In preparation),
	1995

	<li>
	<font color="#ee0000">Paul B. Jackson,</font>
	<b>Enhancing the Nuprl Proof Development System and Applying it to Computational Abstract Algebra,</b>
	Cornell University,
	1994,
	Ithaca, NY,

	<li>
	<font color="#ee0000">Paul B.~Jackson,</font>
	<b>The Nuprl Proof Development System, Version 4.1 Reference Manual and User's Guide,</b>
	Cornell University,
	Ithaca, NY,
	1994

	<li>
	<font color="#ee0000">Paul B. Jackson,</font>
	<i>Exploring Abstract Algebra in Constructive Type Theory</i>,
	<b>12th Conference on Automated Deduction</b>,
	1994,
	A. Bundy (Editor),
	Springer-Verlag,
	New York

	<li>
	<font color="#ee0000">Jackson, Paul B.,</font>
	<i>Developing a toolkit for floating-point hardware in the Nuprl proof development system, </i>
	<b>Advanced Research Workshop on Correct Hardware Design Methodologies,</b>
	pp. 401-419,
	Organized by ESPRIT, Turin, Italy,
	June 1991

	<li>
	<font color="#ee0000">Jackson, Paul B.,</font>
	<i>Nuprl and its Use in Circuit Design, </i>
	<b>Proceedings of the IFIP TC10/WG10.2 
	International Conference on Theorem Provers in Circuit Design: 
	Theory, Practice and Experience, </b> 
	V. Stavridou, T.F. Melham and R.T. Boute (Editors),
	pp. 311-336,
	North-Holland, The Netherlands,
	1992

	<li>
	<font color="#ee0000">Paul B. Jackson,</font>
	<b>Logic-Based Knowledge Representation,</b>
	MIT Press, Cambridge, MA,
	1989

	<li>
        <font color="#ee0000">Knoblock, Ted,</font>
        <b>Mathematical Extensibility in Type Theory</b>,
        Cornell University,
        1987

	<li>
	<font color="#ee0000">Knoblock, Ted B. and Robert L. Constable,</font>
	<i>Formalized Metareasoning in Type Theory,</i>
	<b>Proc. of the First Symp. on Logic in Comp. Sci.,</b>
        pp. 237-248,
	1986,
	IEEE

	<li>
	<font color="#ee0000">Kreitz, Charles,</font>
	<b>Constructive Automata Theory Implemented with the Nuprl Proof Development System,</b>
	Cornell University,
	1986,
	Ithaca, New York

	<li>
	<font color="#ee0000">Kreitz, Charles,</font>
	<b>Meta-Synthesis:  Deriving Programs that Develop Programs,</b>
	Technical University of Darmstadt,
	November, 1992

	<li>
	<font color="#ee0000">O'Leary, John; Miriam Leester; Jason Hickey; and Mark Aagaard,</font>
	<i>Non-Restoring Integer Square Root: A Case Study in Design by Principled Optimization,</i>
	<b>International Conference on Theorem Proving &amp;  Circuit Design,</b>
	1994

	<li>
	<font color="#ee0000">Leeser, Miriam,</font>
	<i>Using Nuprl for the verification and synthesis of hardware,</i>
	<b>Phil. Trans. R. Soc. Lond.</b>,
	1992,
	v. 339,
	pp. 49-68

	<li>
	<font color="#ee0000">Madden, P.,</font>
	<i>Automatic program optimization via the transformation of Nuprl synthesis proofs, </i>
	<b>Proc. of the 1988 Alvey Technical Conf.,</b>
	1988,
	Clarke, L. (Editor),
	(Also available from Edinburgh as DAI Research Paper No. 392)

	<li>
	<font color="#ee0000">Mendler, P.F.</font>
	<i>Recursive Types and Type Constraints in Second-Order Lambda Calculus</i>
	<b>Proc. of Second Symp. on Logic in Comp. Sci.</b>
	IEEE,
	1987,
	pp. 30-36

	<li>
	<font color="#ee0000">Mendler, P.F.,</font>
	<b>Inductive Definition in Type Theory,</b>
	Cornell University,
	Ithaca, NY,
	1988

	<li>
	<font color="#ee0000">Mendler, N.; Robert L.~Constable; and P. Panangaden</font>
	<i>Infinite Objects in Type Theory</i>
	<b>Proc. of First Symp. on Logic in Comp. Sci.</b>
	IEEE,
	1986,
	pp. 249-257
	(Cornell TR 86-743)

	<li>
	<font color="#ee0000">Murthy, Chetan,</font>
	<i>A computational analysis of Girard's translation and LC,</i>
	<b>Proc. of Seventh Symp. on Logic in Comp. Sci.,</b>
	1992

	<li>
	<font color="#ee0000">Murthy, Chetan,</font>
	<i>An Evaluation Semantics for Classical Proofs,</i>
	<b>Proc. of Sixth Symp. on Logic in Comp. Sci.,</b>
	1991,
	pp. 96-109,
	IEEE, Amsterdam, The Netherlands

	<li>
	<font color="#ee0000">Russell, J. and Chetan Murthy,</font>
	<i>A Direct Constructive Proof of Higman's Lemma,</i>
	pp. 257-269,
	<b>Proc. of Fifth Symp. on Logic in Comp. Sci.,</b>
	IEEE,
	1990

	<li>
	<font color="#ee0000">Murthy, Chetan,</font>
	<b>Extracting Constructive Content for Classical Proofs</b>,
	Cornell University, Dept. of Computer Science,
	1990,
	(TR 89-1151)

	<li>
        <font color="#ee0000">Sasaki, James T.,</font>
        <b>The Extraction and Optimization of Programs from Constructive Proofs,</b>
        Cornell University,
        1985

	<li>
        <font color="#ee0000">Smith, Scott F. and Robert L. Constable,</font>
        <i>Partial objects in constructive type theory, </i>
	<b>Proc. of Second Symp. on Logic in Comp. Sci.,</b>
	IEEE, Washington, D.C.,
	pp. 183-93,
        1987
	
	<li>
	<font color="#ee0000">Smith, Scott F.,</font>
	<b>Partial Objects in Type Theory,</b>
	Cornell University,
	Ithaca, NY,
	1989

	<li>
	<font color="#ee0000">J.L. Underwood,</font>
	<b>Aspects of the Computational Content of Proofs,</b>
	Cornell University,
	1994,
	Ithaca, NY
	(Cornell TR94-1460)
	
	<li>
	<font color="#ee0000">Underwood, Judith,</font>
	<i>The Tableau Algorithm for Intuitionistic Propositional 
  	Calculus as a Constructive Completeness Proof</i>,
	<b>Proceedings of the Workshop on Theorem Proving with Analytic Tableaux,</b>
  	Marseille, France,
        pp. 245-248,
	1993,
	(Available as Technical Report MPI-I-93-213
  	Max-Planck-Institut fur Informatik, Saarbrucken, Germany)

	<li>
	<font color="#ee0000">Underwood, Judith,</font>
	<b>A Constructive Completeness Proof for the Intuitionistic Propositional Calculus</b>,
	Cornell University,
	(Cornell TR90-1179),
	1990
    </ol>
    <p>
  <li> <b>Research Papers</b>
    <p>
	<ul>
		<li> <font color="#eeee00">Coming soon
		<li> at your browser!</font>
	</ul>
    <p>
  <li> <b>Research Notes</b>
    <p>
	<ul>
		<li> <font color="#eeee00">Coming soon
		<li> at your browser!</font>
	</ul>
</ul>

<!WA16><!WA16><!WA16><!WA16><!WA16><!WA16><!WA16><!WA16><!WA16><!WA16><!WA16><!WA16><img src="http://www.cs.cornell.edu/Info/Projects/NuPrl/icons/line.red.right.gif">
<p>

<!WA17><!WA17><!WA17><!WA17><!WA17><!WA17><!WA17><!WA17><!WA17><!WA17><!WA17><!WA17><A HREF="http://www.cs.cornell.edu/Info/Projects/NuPrl/index.html"> <!WA18><!WA18><!WA18><!WA18><!WA18><!WA18><!WA18><!WA18><!WA18><!WA18><!WA18><!WA18><IMG SRC="http://www.cs.cornell.edu/Info/Projects/NuPrl/icons/index.gif">
 Return to Main Index </A> <P>

<ADDRESS> Nuprl Project / nuprl@cs.cornell.edu </ADDRESS>

